n  e == n x(*;e) e 

latex

---

clarification:

n g e == n x(*g;eg) e 

latex

Up	groups 1
Wellformedness Lemmas	mon nat op wf, mon nat op wf2
Definitions	n x(op;id) e, *, e